Nuprl Lemma : es-pred!_wf
11,40
postcript
pdf
es
:ES,
e
,
e'
:E. es-pred!(
es
;
e
;
e'
)
latex
Definitions
ES
,
t
T
,
x
:
A
.
B
(
x
)
,
E
,
es-pred?(
es
)
,
es_info(
es
)
,
Id
,
pred!(
e
;
e'
)
,
es-pred!(
es
;
e
;
e'
)
Lemmas
pred!
wf
,
Id
wf
,
es
info
wf
,
es-pred?
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, e, e':E. es-pred!(es;e;e') 
es:ES, e, e':E. es-pred!(es;e;e') Tx:A. B(x)